package edu.uiowa.cs.coqview;

import java.io.IOException;
import java.io.BufferedInputStream;
import java.io.BufferedOutputStream;
import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.InputStreamReader;
import java.io.OutputStreamWriter;

public class CoqtopWrapper {
	private Process ctp;
	private BufferedWriter ctStdInput;
	private BufferedReader ctStdOutput;
	private BufferedReader ctStdError;
	private Thread outGetter;
	private Thread errGetter;
	
	private volatile String outBuffer = "";
	private volatile String errBuffer = "";

	
	
	CoqtopWrapper(String coqtopPath) throws IOException {
		ctp = Runtime.getRuntime().exec(coqtopPath);
		ctStdInput = new BufferedWriter(new
				OutputStreamWriter(new BufferedOutputStream(ctp.getOutputStream())));
		ctStdOutput = new BufferedReader(new
				InputStreamReader(new BufferedInputStream(ctp.getInputStream())));
		ctStdError = new BufferedReader(new
				InputStreamReader(new BufferedInputStream(ctp.getErrorStream())));
		getCtStdOutput();
		getCtStdError();
		
		outGetter = new Thread(this.new CtStdOutputGetter());
		errGetter = new Thread(this.new CtStdErrorGetter(Thread.currentThread()));
		
		outGetter.start();
		errGetter.start();
	}
	
	public void enterCommandGetOutAndErr(String cmd, StringBuffer ctOut, 
			StringBuffer ctErr) {
		
		synchronized(outBuffer) {
			outBuffer = "";
		}
		errBuffer = "";
		
//		if (outGetter != null)
//			if (!outGetter.isAlive())
//				outGetter = new Thread(this.new CtStdOutputGetter());
//		if (outGetter == null)
//			outGetter = new Thread(this.new CtStdOutputGetter());
//		errGetter = new Thread(this.new CtStdErrorGetter(Thread.currentThread()));
		
		try {
			sendToCtStdInput(cmd);	
		} catch (IOException e) {
			System.err.println("IOException occured");
			e.printStackTrace();
		}
		
//		if (!outGetter.isAlive())
//			outGetter.start();
//		errGetter.start();
		try {
			outGetter.join();
			errGetter.join();
		} catch (InterruptedException e) {}
		
		ctOut.replace(0, ctOut.length(), "");
		ctErr.replace(0, ctErr.length(), "");
		synchronized(outBuffer) {
			//System.out.println("/////////////"+outBuffer+"//////////");
			ctOut.append(outBuffer);
		}
		ctErr.append(errBuffer);
		synchronized(outBuffer) {
		outBuffer = "";
		}
		errBuffer = "";
	}
	
	public String getCtStdOutput() throws IOException {
		String s = "";
		do {
			s = s + (char)ctStdOutput.read();
		} while (ctStdOutput.ready());
		return s;
	}
	
	
	
	public String getCtStdError() throws IOException {
		
		//prompt check idea doesn't work:  "\nCoq < " is not always the prompt
		// (e.g. when working on a theorem/lemma)
		char c;
		String s = "";
		//String promptCheck = "asdfghj";
		do {
			c = (char)ctStdError.read();
			s = s + c;
			//promptCheck = promptCheck.substring(1) + c;
			//System.out.println("promptCheck: " + promptCheck);
		} while (ctStdError.ready()); 
				//| !promptCheck.equals("\nCoq < "));
		return s;
	}
	
	public void sendToCtStdInput(String toExecute) throws IOException {
		ctStdInput.write(toExecute);
		ctStdInput.flush();
		return;
	}
	
	private class CtStdOutputGetter implements Runnable {
		public void run() {
			String s = "";
			
			while (true) {
				s = "";
				try {
					s = getCtStdOutput();
				} catch (IOException e) {
					System.err.println("Error occured while getting Coq command response");
				}
				synchronized(outBuffer) {
					outBuffer += s;
				}
			}
			
//			try {
//				while (true) {
//					if (stdOutErrorBuffer[0].equals(""))
//						s = stdOutErrorBuffer[0];
//					s += getCtStdOutput();
//					stdOutErrorBuffer[0] = s;
//				}
//			} catch (IOException e) {
//				System.err.println("Error occurred while getting Coq command response");
//			}
		}
	}
	
	private class CtStdErrorGetter implements Runnable {
		Thread mt;
		CtStdErrorGetter(Thread mainThread) {
			mt = mainThread;
		}
		public void run() {
			while (true) {
				try {
					errBuffer = getCtStdError();
					Thread.sleep(100);
					mt.interrupt();
				} catch (IOException e) {
					System.err.println("Error occured while getting Coq command response");
				} 
				catch (InterruptedException e) {
					
				}
			}
		}
	}
	
	public static void main(String[] args) {
		try {
			CoqtopWrapper ctw = new CoqtopWrapper("/Applications/CoqIdE_8.3.app"+
					"/Contents/Resources/bin/coqtop");
			StringBuffer out = new StringBuffer("");
			StringBuffer err = new StringBuffer("");
			
			String in;
//			in = "Section PropositionalLogic.\n";
//			To do:  enforce \n appending in sendToCtStdInput 
//			ctw.enterCommandGetOutAndErr(in, out, err);
			

			
			//System.out.println(out);
			//System.out.println(err);
			
//			in = "Variable A : Prop.\n";
//			To do:  enforce \n appending in sendToCtStdInput 
//			ctw.enterCommandGetOutAndErr(in, out, err);
			
			//System.out.println(out);
//			System.out.println(err);
			
			for (int i = 0; i < 20; i++) {
				in = "Variable A"+i+" : Prop.\n";
				ctw.enterCommandGetOutAndErr(in, out, err);
				System.out.println(err);
			}
			
		} catch (IOException e) {
			e.printStackTrace();
		}
	}
}
